Relational separation logicYANG, Hongseok.Theoretical computer science. 2007, Vol 375, Num 1-3, pp 308-334, issn 0304-3975, 27 p.Article

Data refinement with low-level pointer operationsMIJAJLOVIC, Ivana; YANG, Hongseok.Lecture notes in computer science. 2005, pp 19-36, issn 0302-9743, isbn 3-540-29735-9, 1Vol, 18 p.Conference Paper

Separation and Information HidingO'HEARN, Peter W; YANG, Hongseok; REYNOLDS, John C et al.ACM transactions on programming languages and systems. 2009, Vol 31, Num 3, issn 0164-0925, 11:1-11:50Article

Modular Verification of Preemptive OS KernelsGOTSMAN, Alexey; YANG, Hongseok.ACM SIGPLAN notices. 2011, Vol 46, Num 9, pp 404-417, issn 1523-2867, 14 p.Conference Paper

Goal-Directed Weakening of Abstract Interpretation ResultsSEO, Sunae; YANG, Hongseok; YI, Kwangkeun et al.ACM transactions on programming languages and systems. 2007, Vol 29, Num 6, issn 0164-0925, 39.1-39.39Article

Automatic verification of pointer programs using grammar-based shape analysisLEE, Oukseh; YANG, Hongseok; YI, Kwangkeun et al.Lecture notes in computer science. 2005, pp 124-140, issn 0302-9743, isbn 3-540-25435-8, 17 p.Conference Paper

Automatic construction of Hoare proofs from abstract interpretation resultsSEO, Sunae; YANG, Hongseok; YI, Kwangkeun et al.Lecture notes in computer science. 2003, pp 230-245, issn 0302-9743, isbn 3-540-20536-5, 16 p.Conference Paper

Inserting safe memory reuse commands into ML-like programsLEE, Oukseh; YANG, Hongseok; YI, Kwangkeun et al.Lecture notes in computer science. 2003, pp 171-188, issn 0302-9743, isbn 3-540-40325-6, 18 p.Conference Paper

Compositional Shape Analysis by Means of Bi-AbductionCALCAGNO, Cristiano; DISTEFANO, Dino; O'HEARN, Peter W et al.Journal of the Association for Computing Machinery. 2011, Vol 58, Num 6, issn 0004-5411, 26.1-26.66Article

Burst-shot infrared digital photography to determine scotopic pupil diameterYANG, Hongseok; LEE, Marvin; JUN BUM KIM et al.Journal of cataract and refractive surgery. 2006, Vol 32, Num 12, pp 2113-2117, issn 0886-3350, 5 p.Article

Step-Indexed Kripke Models over Recursive WorldsBIRKEDAL, Lars; REUS, Bernhard; SCHWINGHAMMER, Jan et al.ACM SIGPLAN notices. 2011, Vol 46, Num 1, pp 119-131, issn 1523-2867, 13 p.Conference Paper

Compositional Shape Analysis by means of Bi-AbductionCALCAGNO, Cristiano; DISTEFANO, Dino; O'HEARN, Peter et al.ACM SIGPLAN notices. 2009, Vol 44, Num 1, pp 289-300, issn 1523-2867, 12 p.Conference Paper

Beyond reachability : Shape abstraction in the presence of pointer arithmeticCALCAGNO, Cristiano; DISTEFANO, Dino; O'HEARN, Peter W et al.Lecture notes in computer science. 2006, pp 182-203, issn 0302-9743, isbn 3-540-37756-5, 1Vol, 22 p.Conference Paper

Abstraction for concurrent objectsFILIPOVIC, Ivana; O'HEARN, Peter; RINETZKY, Noam et al.Theoretical computer science. 2010, Vol 411, Num 51-52, pp 4379-4398, issn 0304-3975, 20 p.Article

A local shape analysis based on separation logicDISTEFANO, Dino; O'HEARN, Peter W; YANG, Hongseok et al.Lecture notes in computer science. 2006, pp 287-302, issn 0302-9743, isbn 3-540-33056-9, 1Vol, 16 p.Conference Paper